KILLED



    


Runtime Complexity (innermost) proof of /tmp/tmp4WPNXl/bubblesort.xml


(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +(S(0), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0
bubble(x, Nil) → Cons(x, Nil)
bsort(0, xs) → xs
bubblesort(xs) → bsort(len(xs), xs)

The (relative) TRS S consists of the following rules:

+(x, S(0)) → S(x)
+(S(0), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)

The (relative) TRS S consists of the following rules:

+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
bsort, bubble, len, <

They will be analysed ascendingly in the following order:
bubble < bsort
< < bubble

(6) Obligation:

Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

The following defined symbols remain to be analysed:
len, bsort, bubble, <

They will be analysed ascendingly in the following order:
bubble < bsort
< < bubble

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)

Induction Base:
len(gen_Cons:Nil4_0(0)) →RΩ(1)
0'

Induction Step:
len(gen_Cons:Nil4_0(+(n7_0, 1))) →RΩ(1)
+'(S(0'), len(gen_Cons:Nil4_0(n7_0))) →IH
+'(S(0'), gen_S:0'5_0(c8_0)) →RΩ(0)
S(gen_S:0'5_0(n7_0))

We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

The following defined symbols remain to be analysed:
<, bsort, bubble

They will be analysed ascendingly in the following order:
bubble < bsort
< < bubble

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
<(gen_S:0'5_0(n417_0), gen_S:0'5_0(+(1, n417_0))) → True, rt ∈ Ω(0)

Induction Base:
<(gen_S:0'5_0(0), gen_S:0'5_0(+(1, 0))) →RΩ(0)
True

Induction Step:
<(gen_S:0'5_0(+(n417_0, 1)), gen_S:0'5_0(+(1, +(n417_0, 1)))) →RΩ(0)
<(gen_S:0'5_0(n417_0), gen_S:0'5_0(+(1, n417_0))) →IH
True

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)
<(gen_S:0'5_0(n417_0), gen_S:0'5_0(+(1, n417_0))) → True, rt ∈ Ω(0)

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

The following defined symbols remain to be analysed:
bubble, bsort

They will be analysed ascendingly in the following order:
bubble < bsort

(13) Obligation:

Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)
<(gen_S:0'5_0(n417_0), gen_S:0'5_0(+(1, n417_0))) → True, rt ∈ Ω(0)

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

No more defined symbols left to analyse.

(14) Obligation:

Innermost TRS:
Rules:
bsort(S(x'), Cons(x, xs)) → bsort(x', bubble(x, xs))
len(Cons(x, xs)) → +'(S(0'), len(xs))
bubble(x', Cons(x, xs)) → bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
len(Nil) → 0'
bubble(x, Nil) → Cons(x, Nil)
bsort(0', xs) → xs
bubblesort(xs) → bsort(len(xs), xs)
+'(x, S(0')) → S(x)
+'(S(0'), y) → S(y)
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
bubble[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, bubble(x', xs))
bubble[Ite][False][Ite](True, x', Cons(x, xs)) → Cons(x', bubble(x, xs))

Types:
bsort :: S:0' → Cons:Nil → Cons:Nil
S :: S:0' → S:0'
Cons :: S:0' → Cons:Nil → Cons:Nil
bubble :: S:0' → Cons:Nil → Cons:Nil
len :: Cons:Nil → S:0'
+' :: S:0' → S:0' → S:0'
0' :: S:0'
bubble[Ite][False][Ite] :: True:False → S:0' → Cons:Nil → Cons:Nil
< :: S:0' → S:0' → True:False
Nil :: Cons:Nil
bubblesort :: Cons:Nil → Cons:Nil
True :: True:False
False :: True:False
hole_Cons:Nil1_0 :: Cons:Nil
hole_S:0'2_0 :: S:0'
hole_True:False3_0 :: True:False
gen_Cons:Nil4_0 :: Nat → Cons:Nil
gen_S:0'5_0 :: Nat → S:0'

Lemmas:
len(gen_Cons:Nil4_0(n7_0)) → gen_S:0'5_0(n7_0), rt ∈ Ω(1 + n70)

Generator Equations:
gen_Cons:Nil4_0(0) ⇔ Nil
gen_Cons:Nil4_0(+(x, 1)) ⇔ Cons(0', gen_Cons:Nil4_0(x))
gen_S:0'5_0(0) ⇔ 0'
gen_S:0'5_0(+(x, 1)) ⇔ S(gen_S:0'5_0(x))

No more defined symbols left to analyse.